module testbench (
	input clk, reset
);
	`RVFI_WIRES

	`RVFI_CHANNEL(rvfi_ch0, 0)
	`RVFI_CHANNEL(rvfi_ch1, 1)

`ifdef YOSYS
	assume property (reset == $initstate);
`endif

	rvfi_wrapper uut (
		.clock (clk  ),
		.reset (reset),
		`RVFI_CONN
	);

	wire valid_ch0;
	wire valid_ch1;

	riscv_rv64ic_insn riscv_rv64ic_insn_ch0 (
		.insn(rvfi_insn_ch0),
		.valid(valid_ch0)
	);

	riscv_rv64ic_insn riscv_rv64ic_insn_ch1 (
		.insn(rvfi_insn_ch1),
		.valid(valid_ch1)
	);

	function [0:0] check_insn;
		input [31:0] insn;
		begin
			check_insn = 0;
			casez (insn)
				32'b 0000000000000000_010_?00000?????_10:; // C.LWSP (fix pending)
				32'b 0000000000000000_011_?00000?????_10:; // C.LDSP (fix pending)
				32'b ???????_?????_?????_???_?????_1110011:; // SYSTEM
				32'b ???????_?????_?????_000_?????_0001111:; // FENCE
				32'b ???????_?????_?????_001_?????_0001111:; // FENCE.I
				32'b 00010??_00000_?????_???_?????_0101111:; // LR.W
				32'b 00011??_?????_?????_???_?????_0101111:; // SC.W
				32'b 00001??_?????_?????_???_?????_0101111:; // AMOSWAP.W
				32'b 00000??_?????_?????_???_?????_0101111:; // AMOADD.W
				32'b 00100??_?????_?????_???_?????_0101111:; // AMOXOR.W
				32'b 01100??_?????_?????_???_?????_0101111:; // AMOAND.W
				32'b 01000??_?????_?????_???_?????_0101111:; // AMOOR.W
				32'b 10000??_?????_?????_???_?????_0101111:; // AMOMIN.W
				32'b 10100??_?????_?????_???_?????_0101111:; // AMOMAX.W
				32'b 11000??_?????_?????_???_?????_0101111:; // AMOMINU.W
				32'b 11100??_?????_?????_???_?????_0101111:; // AMOMAXU.W
				default: check_insn = 1;
			endcase
		end
	endfunction

	wire check_insn_ch0 = check_insn(rvfi_insn_ch0);
	wire check_insn_ch1 = check_insn(rvfi_insn_ch1);

	always @* begin
		if (!reset && rvfi_valid_ch0 && check_insn_ch0 && !rvfi_trap_ch0) begin
			assert (valid_ch0);
		end
		if (!reset && rvfi_valid_ch1 && check_insn_ch1 && !rvfi_trap_ch1) begin
			assert (valid_ch1);
		end
	end
endmodule
